(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

0(1(1(2(x1)))) → 1(3(0(1(2(x1)))))
0(1(1(2(x1)))) → 1(3(1(0(2(x1)))))
0(1(1(2(x1)))) → 2(3(1(3(0(1(x1))))))
0(1(2(0(x1)))) → 1(0(0(2(2(x1)))))
0(1(2(4(x1)))) → 0(2(3(4(1(x1)))))
0(1(2(4(x1)))) → 1(0(4(2(3(x1)))))
0(1(2(4(x1)))) → 1(2(3(0(4(x1)))))
0(1(2(4(x1)))) → 2(1(4(0(3(x1)))))
0(1(2(4(x1)))) → 1(2(3(4(0(5(x1))))))
0(1(2(4(x1)))) → 2(1(1(0(3(4(x1))))))
0(1(2(4(x1)))) → 4(1(2(2(3(0(x1))))))
0(1(2(4(x1)))) → 4(5(0(2(3(1(x1))))))
0(4(2(0(x1)))) → 0(4(2(3(0(x1)))))
0(4(2(0(x1)))) → 2(3(0(4(0(0(x1))))))
0(4(2(0(x1)))) → 3(4(0(2(3(0(x1))))))
0(4(2(0(x1)))) → 4(2(3(0(4(0(x1))))))
0(4(2(0(x1)))) → 4(3(0(0(5(2(x1))))))
0(4(2(4(x1)))) → 4(0(2(3(1(4(x1))))))
0(4(2(4(x1)))) → 4(0(4(2(0(3(x1))))))
5(1(2(0(x1)))) → 2(1(3(5(0(x1)))))
5(1(2(0(x1)))) → 3(1(0(2(5(x1)))))
5(1(2(0(x1)))) → 2(3(0(0(1(5(x1))))))
5(1(2(4(x1)))) → 3(2(5(1(4(x1)))))
5(1(2(4(x1)))) → 5(2(1(3(4(x1)))))
5(1(2(4(x1)))) → 5(5(2(1(4(x1)))))
5(1(2(4(x1)))) → 0(3(4(5(2(1(x1))))))
5(1(4(2(x1)))) → 3(4(5(2(1(x1)))))
5(1(4(2(x1)))) → 2(1(3(4(5(4(x1))))))
5(1(4(2(x1)))) → 3(3(4(2(1(5(x1))))))
5(4(1(4(x1)))) → 3(4(4(1(5(4(x1))))))
5(4(1(4(x1)))) → 4(1(3(5(0(4(x1))))))
5(4(1(4(x1)))) → 5(1(3(4(5(4(x1))))))
5(4(1(4(x1)))) → 5(1(5(3(4(4(x1))))))
5(4(2(0(x1)))) → 5(4(2(3(0(x1)))))
5(4(2(0(x1)))) → 0(1(2(3(4(5(x1))))))
5(4(2(0(x1)))) → 4(5(3(3(0(2(x1))))))
0(1(2(0(4(x1))))) → 0(2(4(1(3(0(x1))))))
0(1(2(0(4(x1))))) → 2(0(3(4(0(1(x1))))))
0(1(2(0(4(x1))))) → 4(0(2(3(1(0(x1))))))
0(1(4(2(2(x1))))) → 1(2(3(4(0(2(x1))))))
5(0(1(2(4(x1))))) → 3(0(2(1(4(5(x1))))))
5(1(2(2(4(x1))))) → 5(2(2(1(4(5(x1))))))
5(1(2(4(0(x1))))) → 5(0(2(1(3(4(x1))))))
5(1(2(4(0(x1))))) → 5(0(3(2(1(4(x1))))))
5(1(3(1(4(x1))))) → 1(5(1(3(4(0(x1))))))
5(1(4(1(2(x1))))) → 2(1(5(3(4(1(x1))))))
5(4(1(1(4(x1))))) → 1(1(3(4(5(4(x1))))))
5(4(1(4(0(x1))))) → 3(4(0(4(5(1(x1))))))
5(4(3(2(0(x1))))) → 5(4(0(3(2(3(x1))))))
5(4(5(2(0(x1))))) → 5(0(5(4(4(2(x1))))))

Rewrite Strategy: INNERMOST

(1) CpxTrsMatchBoundsProof (EQUIVALENT transformation)

A linear upper bound on the runtime complexity of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 2.
The certificate found is represented by the following graph.
Start state: 4591
Accept states: [4592, 4593]
Transitions:
4591→4592[0_1|0]
4591→4593[5_1|0]
4591→4591[1_1|0, 2_1|0, 3_1|0, 4_1|0]
4591→4594[2_1|1]
4591→4598[2_1|1]
4591→4602[1_1|1]
4591→4607[1_1|1]
4591→4612[1_1|1]
4591→4616[4_1|1]
4591→4621[5_1|1]
4591→4626[2_1|1]
4591→4631[1_1|1]
4591→4635[3_1|1]
4591→4639[4_1|1]
4591→4643[3_1|1]
4591→4647[5_1|1]
4591→4652[4_1|1]
4591→4657[0_1|1]
4591→4662[1_1|1]
4591→4667[4_1|1]
4591→4671[4_1|1]
4591→4675[4_1|1]
4591→4679[1_1|1]
4591→4684[4_1|1]
4591→4689[3_1|1]
4591→4694[5_1|1]
4591→4699[4_1|1]
4591→4704[4_1|1]
4591→4709[4_1|1]
4591→4714[4_1|1]
4591→4719[0_1|1]
4591→4724[4_1|1]
4594→4595[1_1|1]
4595→4596[0_1|1]
4596→4597[3_1|1]
4597→4592[1_1|1]
4597→4657[1_1|1]
4597→4719[1_1|1]
4597→4603[1_1|1]
4598→4599[0_1|1]
4599→4600[1_1|1]
4600→4601[3_1|1]
4601→4592[1_1|1]
4601→4657[1_1|1]
4601→4719[1_1|1]
4601→4603[1_1|1]
4602→4603[0_1|1]
4603→4604[3_1|1]
4604→4605[1_1|1]
4605→4606[3_1|1]
4606→4592[2_1|1]
4606→4657[2_1|1]
4606→4719[2_1|1]
4606→4603[2_1|1]
4607→4608[4_1|1]
4608→4609[3_1|1]
4609→4610[5_1|1]
4610→4611[1_1|1]
4611→4593[2_1|1]
4611→4621[2_1|1]
4611→4647[2_1|1]
4611→4694[2_1|1]
4611→4669[2_1|1]
4612→4613[2_1|1]
4613→4614[5_1|1]
4614→4615[4_1|1]
4615→4593[3_1|1]
4615→4621[3_1|1]
4615→4647[3_1|1]
4615→4694[3_1|1]
4615→4669[3_1|1]
4616→4617[5_1|1]
4617→4618[4_1|1]
4618→4619[3_1|1]
4619→4620[1_1|1]
4620→4593[2_1|1]
4620→4621[2_1|1]
4620→4647[2_1|1]
4620→4694[2_1|1]
4620→4669[2_1|1]
4621→4622[1_1|1]
4622→4623[2_1|1]
4623→4624[4_1|1]
4624→4625[3_1|1]
4625→4593[3_1|1]
4625→4621[3_1|1]
4625→4647[3_1|1]
4625→4694[3_1|1]
4625→4669[3_1|1]
4626→4627[0_1|1]
4627→4628[4_1|1]
4628→4629[3_1|1]
4629→4630[2_1|1]
4630→4592[1_1|1]
4630→4657[1_1|1]
4630→4719[1_1|1]
4630→4603[1_1|1]
4631→4632[4_1|1]
4632→4633[3_1|1]
4633→4634[2_1|1]
4634→4592[0_1|1]
4634→4657[0_1|1]
4634→4719[0_1|1]
4634→4603[0_1|1]
4634→4596[0_1|1]
4635→4636[2_1|1]
4636→4637[4_1|1]
4637→4638[0_1|1]
4638→4592[1_1|1]
4638→4657[1_1|1]
4638→4719[1_1|1]
4638→4603[1_1|1]
4638→4596[1_1|1]
4639→4640[0_1|1]
4640→4641[3_1|1]
4641→4642[2_1|1]
4642→4592[1_1|1]
4642→4657[1_1|1]
4642→4719[1_1|1]
4642→4603[1_1|1]
4642→4596[1_1|1]
4643→4644[0_1|1]
4644→4645[4_1|1]
4645→4646[1_1|1]
4646→4592[2_1|1]
4646→4657[2_1|1]
4646→4719[2_1|1]
4646→4603[2_1|1]
4646→4596[2_1|1]
4647→4648[0_1|1]
4648→4649[4_1|1]
4649→4650[3_1|1]
4650→4651[2_1|1]
4651→4592[1_1|1]
4651→4657[1_1|1]
4651→4719[1_1|1]
4651→4603[1_1|1]
4651→4596[1_1|1]
4652→4653[3_1|1]
4653→4654[0_1|1]
4654→4655[1_1|1]
4655→4656[1_1|1]
4656→4592[2_1|1]
4656→4657[2_1|1]
4656→4719[2_1|1]
4656→4603[2_1|1]
4656→4596[2_1|1]
4657→4658[3_1|1]
4658→4659[2_1|1]
4659→4660[2_1|1]
4660→4661[1_1|1]
4661→4592[4_1|1]
4661→4657[4_1|1]
4661→4719[4_1|1]
4661→4603[4_1|1]
4661→4596[4_1|1]
4662→4663[3_1|1]
4663→4664[2_1|1]
4664→4665[0_1|1]
4665→4666[5_1|1]
4666→4592[4_1|1]
4666→4657[4_1|1]
4666→4719[4_1|1]
4666→4603[4_1|1]
4666→4596[4_1|1]
4667→4668[1_1|1]
4668→4669[5_1|1]
4669→4670[2_1|1]
4670→4593[3_1|1]
4670→4621[3_1|1]
4670→4647[3_1|1]
4670→4694[3_1|1]
4671→4672[3_1|1]
4672→4673[1_1|1]
4673→4674[2_1|1]
4674→4593[5_1|1]
4674→4621[5_1|1]
4674→4647[5_1|1]
4674→4694[5_1|1]
4675→4676[1_1|1]
4676→4677[2_1|1]
4677→4678[5_1|1]
4678→4593[5_1|1]
4678→4621[5_1|1]
4678→4647[5_1|1]
4678→4694[5_1|1]
4679→4680[2_1|1]
4680→4681[5_1|1]
4681→4682[4_1|1]
4682→4683[3_1|1]
4683→4593[0_1|1]
4683→4621[0_1|1]
4683→4647[0_1|1]
4683→4694[0_1|1]
4684→4685[1_1|1]
4685→4686[3_1|1]
4686→4687[2_1|1]
4687→4688[0_1|1]
4688→4592[4_1|1]
4688→4657[4_1|1]
4688→4719[4_1|1]
4688→4640[4_1|1]
4688→4705[4_1|1]
4689→4690[0_1|1]
4689→4730[0_1|2]
4689→4734[0_1|2]
4689→4739[0_1|2]
4689→4744[0_1|2]
4689→4749[2_1|2]
4690→4691[2_1|1]
4691→4692[4_1|1]
4692→4693[0_1|1]
4693→4592[4_1|1]
4693→4657[4_1|1]
4693→4719[4_1|1]
4693→4640[4_1|1]
4693→4705[4_1|1]
4694→4695[4_1|1]
4695→4696[1_1|1]
4696→4697[2_1|1]
4697→4698[2_1|1]
4698→4593[5_1|1]
4698→4621[5_1|1]
4698→4647[5_1|1]
4698→4694[5_1|1]
4699→4700[5_1|1]
4700→4701[1_1|1]
4701→4702[4_1|1]
4702→4703[4_1|1]
4703→4593[3_1|1]
4703→4621[3_1|1]
4703→4647[3_1|1]
4703→4694[3_1|1]
4703→4617[3_1|1]
4703→4700[3_1|1]
4703→4710[3_1|1]
4703→4725[3_1|1]
4704→4705[0_1|1]
4705→4706[5_1|1]
4706→4707[3_1|1]
4707→4708[1_1|1]
4708→4593[4_1|1]
4708→4621[4_1|1]
4708→4647[4_1|1]
4708→4694[4_1|1]
4708→4617[4_1|1]
4708→4700[4_1|1]
4708→4710[4_1|1]
4708→4725[4_1|1]
4709→4710[5_1|1]
4710→4711[4_1|1]
4711→4712[3_1|1]
4712→4713[1_1|1]
4713→4593[5_1|1]
4713→4621[5_1|1]
4713→4647[5_1|1]
4713→4694[5_1|1]
4713→4617[5_1|1]
4713→4700[5_1|1]
4713→4710[5_1|1]
4713→4725[5_1|1]
4714→4715[4_1|1]
4715→4716[3_1|1]
4716→4717[5_1|1]
4717→4718[1_1|1]
4718→4593[5_1|1]
4718→4621[5_1|1]
4718→4647[5_1|1]
4718→4694[5_1|1]
4718→4617[5_1|1]
4718→4700[5_1|1]
4718→4710[5_1|1]
4718→4725[5_1|1]
4719→4720[4_1|1]
4720→4721[3_1|1]
4721→4722[1_1|1]
4722→4723[5_1|1]
4723→4593[1_1|1]
4723→4621[1_1|1]
4723→4647[1_1|1]
4723→4694[1_1|1]
4724→4725[5_1|1]
4725→4726[4_1|1]
4726→4727[3_1|1]
4727→4728[1_1|1]
4728→4593[1_1|1]
4728→4621[1_1|1]
4728→4647[1_1|1]
4728→4694[1_1|1]
4728→4617[1_1|1]
4728→4700[1_1|1]
4728→4710[1_1|1]
4728→4725[1_1|1]
4730→4731[3_1|2]
4731→4732[2_1|2]
4732→4733[4_1|2]
4733→4693[0_1|2]
4734→4735[0_1|2]
4735→4736[4_1|2]
4736→4737[0_1|2]
4737→4738[3_1|2]
4738→4693[2_1|2]
4739→4740[3_1|2]
4740→4741[2_1|2]
4741→4742[0_1|2]
4742→4743[4_1|2]
4743→4693[3_1|2]
4744→4745[4_1|2]
4745→4746[0_1|2]
4746→4747[3_1|2]
4747→4748[2_1|2]
4748→4693[4_1|2]
4749→4750[5_1|2]
4750→4751[0_1|2]
4751→4752[0_1|2]
4752→4753[3_1|2]
4753→4693[4_1|2]

(2) BOUNDS(O(1), O(n^1))